Row polymorphismとstructural subtypingの違い
擬似コードをgpt-4.iconに書かせて理解しようと思ったけど、これ疑似TypeScriptじゃだめだなmrsekut.icon
実行時に型情報を見て挙動が変わるようなものを想定しないと理解がおかしくなる
GPT-4.icon
見た目は同じ「余計なフィールドを許す」振る舞いでも、
structural subtyping は 部分型関係（≤）
row polymorphism は 型変数の量化・具体化（∀・instantiation）
という 全く別の原理に基づいている。
1. 中核の違い：≤ か ∀ か
Structural subtyping
より情報が多い型（フィールドが多い）ほど、より一般の型（フィールドが少ない）としても使える
例：{x:Int, y:Int} ≤ {x:Int}
だから {x:Int, y:Int} を {x:Int} として渡せる
サブタイプ関係（≤） による upcast が本質
Row polymorphism
必要なフィールド以外は未知として抽象化する
例：f : ∀r. {x:Int | r} -> Int
x以外に何があっても良い
f {x:1, c:100}とした時、r := { c:Int }となる
つまり、
サブタイプに変換されるのではなく
型変数が具体化される
Subtyping なら必要なのはこの規則だけ：
code:text
T₁ ≤ T₂ ⇒ t : T₂
しかし row polymorphism では：
{x,c} が {x|r} のサブタイプではない
代わりに r を {c} に instantiationしている
つまり：
部分型関係（≤）が存在しない
subsumption を導出できない
→ だから row polymorphism ≠ subtyping
2. 余計なフィールドを受け入れる理由の違い
Structural subtypingの理由
引数位置で「より具体的なもの（フィールド多い）」は「より抽象的な要求（フィールド少ない）」を満たす
→ だから渡せる（置換原理）
Row polymorphismの理由
型が最初から「残り r は何でもよい」と言っている
→ だから受ける側の型が“開いている”
3. 決定的な違い（レコードを返す関数）
Structural subtyping
引数で {a,b,c} → {a,b} に upcast
余分な c は 型から忘れられる
結果：c は保持できない
Row polymorphism
{a,b | ρ} に {a,b,c} を渡すと ρ := {c}
ρ が計算後も保持される
結果：c を含んだまま拡張できる
👉
情報を捨てるか（subtyping）／保持するか（row polymorphism） が本質差。
4. 型推論への影響
Structural subtyping
制約に ≤ が入りやすい
join / meet / 制約解決が絡む
HM 型推論と組み合わせると設計が難しい
Row polymorphism
row 変数の単一化が中心
必要なフィールドが型に露出する
HM に近い推論で扱いやすい
5. まとめ表
table:_
観点 Structural subtyping Row polymorphism
原理 部分型関係（≤） 多相性（∀・型変数）
余剰フィールド 捨てられる 保持される
メカニズム upcast / subsumption instantiation
情報保存 苦手 得意
推論 難しい 比較的容易
6. 決定的な違いが出る例（重要）
コード
code:js
let f x = x with { sum: x.a + x.b }
let answer = f {a:1, b:2, c:100}
Structural subtyping の場合
1. 引数は {a,b,c}
2. {a,b} に upcast
3. f は {a,b} だけを知っている
結果の型：
code:text
answer :: { a : Number, b : Number, sum : Number }
c が消える
理由：
入力時点で型から忘れられたため
型システム的に「保持できない」
Row polymorphism の場合
1. 型は { a, b | ρ }
2. ρ := { c : Number }
3. レコード拡張後も ρ は保持される
結果の型：
code:text
answer :: { a : Number, b : Number, c : Number, sum : Number }
c が保存される
8. なぜ「誰が気にするのか？」
Subtyping と型推論は相性が悪い
一般的な subtyping + HM 型推論 → 複雑・非決定的
Row polymorphism → 単一化ベースで推論可能
つまり：
型推論を持つ言語
レコードを安全に扱いたい
なら、
structural subtyping ではなく row polymorphism を選ぶべき